PRISM
=====
Version: 4.5.dev
Date: Sat Mar 14 11:34:27 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -mtbdd -e 1e-6 -maxiters 1000000 bluetooth.prism bluetooth.props --property time -const mrec=1
Parsing model file "bluetooth.prism"...
Type: DTMC
Modules: receiver1 frequency1 sender_frequency replies
Variables: y1 receiver freq1 train1 z1 f1 t1 send freq train c rep rec
Parsing properties file "bluetooth.props"...
1 property:
(1) "time": filter(max, R=? [ F rec=mrec ], "init")
---------------------------------------------------------------------
Model checking: "time": filter(max, R=? [ F rec=mrec ], "init")
Model constants: mrec=1
Building model...
Model constants: mrec=1
Computing reachable states...
Reachability (BFS): 50 iterations in 0.16 seconds (average 0.003200, setup 0.00)
Time for model construction: 11.332 seconds.
Type: DTMC
States: 3411945339 (536870912 initial)
Transitions: 5035263739
Transition matrix: 14727 nodes (4 terminal), 5035263739 minterms, vars: 52r/52c
Prob0: 49 iterations in 0.62 seconds (average 0.012653, setup 0.00)
Prob1: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00)
goal = 1636000575, inf = 0, maybe = 1775944764
Computing remaining rewards...
Engine: MTBDD
Iteration matrix MTBDD... [nodes=11441] [223.5 Kb]
Diagonals MTBDD... [nodes=4425] [86.4 Kb]
Starting iterations...
Jacobi: 47 iterations in 0.54 seconds (average 0.011277, setup 0.01)
Maximum value over states satisfying filter: 8229.0
There are 32768 states with (approximately) this value.
The first 10 states are displayed below. To view them all, enable verbose mode or use a print filter.
4479:(0,0,0,0,1,1,0,1,2,0,3,128,0)
4735:(0,0,0,0,1,1,0,1,2,0,5,128,0)
4991:(0,0,0,0,1,1,0,1,2,0,7,128,0)
5247:(0,0,0,0,1,1,0,1,2,0,9,128,0)
5503:(0,0,0,0,1,1,0,1,2,0,11,128,0)
5759:(0,0,0,0,1,1,0,1,2,0,13,128,0)
6015:(0,0,0,0,1,1,0,1,2,0,15,128,0)
6271:(0,0,0,0,1,1,0,1,2,1,1,128,0)
233777:(0,0,0,0,2,1,0,1,2,0,3,128,0)
234033:(0,0,0,0,2,1,0,1,2,0,5,128,0)
Time for model checking: 0.886 seconds.
Result: 8229.0 (maximum value over states satisfying filter)
Overall running time: 12.843 seconds.